rcv($l$,${\it tg}$) declared in $M$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}dom(KindDeq; rcv($l$,${\it tg}$); 1of(2of($M$)))